(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Soundness                           *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions Scalina_SubstFresh Scalina_Induction Scalina_Regularity Scalina_Env support.
Require Import List.

Hint Constructors typing wf_tp wf_mem wf_mems concrete_tp concrete_mem expand.

(* ********************************************************************** *)
(** * Proofs *)

(** Typing is preserved by weakening. *)

Lemma typing_weaken : forall E F,
 (forall H (t : tm) (T : tp),
    H |= t ~: T -> forall G, H = E & G -> wf_env (E & F & G) -> (E & F & G) |= t ~: T ) /\
 (forall H (T : tp),
    H |= T ~::Struct -> forall G, H = (E & G) -> wf_env (E & F & G) -> (E & F & G) |= T ~::Struct ) /\
 (forall H (T : tp),
    H |= T ~::Concrete -> forall G, H = (E & G) -> wf_env (E & F & G) -> (E & F & G) |= T ~::Concrete) /\
 (forall H (T R: tp),
    H |= T ~< R -> forall G, H = (E & G) -> wf_env (E & F & G) -> (E & F & G) |= T ~< R) /\
 (forall H, 
    wf_env H -> forall G, H = (E & G) -> wf_env (E & F & G) -> wf_env (E & F & G)) /\
 (forall H (m : mem),
    H |= m ~:::wf -> forall G, H = (E & G) -> wf_env (E & F & G) -> (E & F & G) |= m ~:::wf) /\
 (forall H (ms : list mem),
    H |= ms ~:::wfs -> forall G, H = (E & G) -> wf_env (E & F & G) -> (E & F & G) |= ms ~:::wfs).
Proof.
 intros. 

  (* did this manually: gen_eq (E & G) as H. gen G., don't know how to do it inside the conjunctions *)
 apply typing_wf_mutual_ind; intro H; intros; subst; auto*.

(* case var *)
  apply* typing_var. apply* binds_weaken. 
  apply (wf_env_implies_ok H2).
  
  apply_fresh wf_struct_self as x; trivial. (* only works if wf_struct_self's first quantified variable is L, and its first hypothesis is the freshness hypo. *)
   apply H0 with (x:= x) (G0:= G & x ~ SelfTp); auto*. 
     assert (x \notin H) as FrH by auto*.
     pose (w':= w x FrH). clear H0.
     destruct typing_regular as [_ [_ [_ [_ [_ [_ TypReg]]]]]].
     destruct (TypReg _ (open_mems ms x) w') as [HWf _]. simpl_env. clear TypReg w' FrH w l.

      assert (x # F) as FrX by auto*.
      apply (splice_wf_env _ _ _ H3 HWf FrX).
      apply (H1 G); trivial.
Qed.

Lemma member_lookup_preserves_fv: forall (o: option tp) (mems : list mem) (l : lab) (T : tp) t x,
 x \notin fv_tp (tp_struct o mems) -> option_has T (mems ?: l) -> x \notin fv_tm t
 -> x \notin fv_tp ({0 ~tp> t}T).
Proof. 
  intros.

  functional induction (mems_lookup l mems); simpl in H0.
    contradiction.
    subst T. functional induction (mem_getLabel m'). 
     induction o; repeat(
       simpl; simpl in H; assert (x \notin fold_left (fun (ats : vars) (m : mem) => ats \u fv_mem m) E' ({} \u (fv_tp _x0 \u option_fold fv_tm {} _x1))) as NI by auto*;
       replace (fv_tp _x0 \u option_fold fv_tm {} _x1) with (fv_mem (mtm l0 mut0 _x0 _x1)) in NI by auto*;
       rewrite foldUnionAssoc in NI; simpl in NI; assert (x \notin fv_tp _x0) by auto*;
       destruct (fv_open_var_conv _ H1) as [_ [OpenTp _]]; apply OpenTp; trivial).

     apply IHo0; auto*. simpl. simpl in H. rewrite foldUnionAssoc in H. auto*.
Qed.



Lemma typing_fresh: forall x,
    (forall E t T,
      E |= t ~: T -> x \notin dom E -> x \notin fv_tm t /\ x \notin fv_tp T) /\
    (forall E T,
      E |= T ~::Struct ->  x \notin dom E -> x \notin fv_tp T) /\
    (forall E T,
      E |= T ~::Concrete -> True) /\
    (forall E T R,
      E |= T ~< R -> True) /\
    (forall E,
      wf_env E ->  True) /\
    (forall E m,
      E |= m ~:::wf -> x \notin dom E -> x \notin fv_mem m) /\
    (forall E ms,
      E |= ms ~:::wfs -> x \notin dom E -> x \notin fv_mems ms).
Proof.
  introv.
  apply typing_wf_mutual_ind; try intro H; intros; subst; simpl; auto*.

  split. 
    destruct (x == x0). subst. contradiction (binds_fresh b). auto.
    apply (@wf_env_inv_type_dep _ _ _ x w b H1); trivial.

(* typing_sel *) 
  split. destructs (H0 H1); trivial.
  clear t.
  functional induction (mems_lookup l mems).
    contradiction o0. 
    simpl in *. functional induction (mem_getClassifier m'). simpl in _x. rename H0 into IHTyp. simpl in IHTyp.
    destruct (IHTyp H1) as [_ XNotin]. 
    assert (x \notin fold_left (fun (ats : vars) (m : mem) => ats \u fv_mem m) E'
            ({} \u (fv_tp T \u option_fold fv_tm {} _x0))) by auto*.

    pose (notin_fold_left_monotone _ _ H0).
    auto.
    apply IHo1; auto*. intros.
    pose (Hnotin:= H0 H2). simpl in Hnotin.
    rewrite (notin_union x (option_fold fv_tp {} o) (fold_left (fun (ats : vars) (m : mem) => ats \u fv_mem m) (m' :: E') {})) in Hnotin.
    destruct Hnotin as [HNItm [HNIA HNIB]].
    pose (notin_fold_left_monotone2 _ E' fv_mem HNIB). 
    simpl.
    auto*.

(* typing_sel_single *)
  destructs (H0 H1). split; trivial.
  eapply member_lookup_preserves_fv; eauto.

(* typing_new *)
   inversions* e. 


(**)
   fold (fv_mems ms).
   pick_fresh y.  assert ( x \notin fv_mems (open_mems ms y)) by auto*. assert (x <> y) as DiffXY by auto.
     destruct (fv_open_var DiffXY) as [_ [_ [_ FOVMems]]].
     pose (FM:= FOVMems ms 0 H3).  pose (H1 H2). notin_solve.

   fold (fv_mems ms).
   pick_fresh y. pose (H':= H0 H1).  simpl in H'. fold (fv_mems ms) in H'. notin_solve.

  notin_simpl; pose (H0 H1); auto*.
  notin_simpl; pose (H1 H2); auto*.
  compute. auto.
  pose (H0 H2).  pose (H1 H2).
  unfold fv_mems in *. simpl. 
  rewrite (foldUnionAssoc fv_mem ms m).
  notin_simpl; trivial.
Qed.



(** helper lemma's for typing_subst **)

Lemma subst_distr_lookup: forall u T l mems z,
     lc_tm u
  -> option_has T (mems ?: l)
  -> option_has ([z ~tp> u]T) (([z ~mems> u]mems) ?: l).
Proof.
  intros.

  functional induction (mems_lookup l mems). contradiction. simpl.
    functional induction (mem_getLabel m'). unfold mem_getClassifier. simpl in *. rewrite <- _x in *.  subst _x0.
      induction (eq_lab_dec l l).
        simpl. trivial.
        destruct e0. assert (l=l) by reflexivity. contradiction.
    simpl in *. 
    replace (mem_getLabel ([z ~mem> u]m')) with (mem_getLabel m'). 
    induction e0. destruct (eq_lab_dec l (mem_getLabel m')). 
      contradiction.
      apply IHo; assumption.
    
    unfold mem_getLabel. induction m'. simpl. trivial.
Qed.


Lemma subst_dist_concrete_mems: forall ms z u,
    lc_tm u
 -> list_forAll (map concrete_mem ms)
 -> list_forAll (map concrete_mem ([z ~mems> u]ms)).
Proof.
  introv HLc HAll. induction ms. simpl in *. trivial. simpl. simpl in HAll. destruct HAll. split. 
  induction a. simpl. inversion H. subst. simpl.
  apply concrete_mem_tm. destruct (@subst_lc z u HLc) as [Hlc _]. apply Hlc; assumption.
  apply* IHms.
Qed.

Lemma subst_distr_memin: forall u m ms z,
  lc_tm u ->
  ~ MemIn m ms -> ~ MemIn ([z ~mem> u]m) ([z ~mems> u]ms). 
Proof.
  intros.
  unfold not in *.
  intros.
  unfold MemIn in *.
  unfold subst_mems in H1. rewrite map_map in H1.
Lemma subst_distr_mem_getLabel: forall u z,
  lc_tm u ->
  (forall m, mem_getLabel m = mem_getLabel ([z ~mem> u]m)).
Proof.
  intros. 
  functional induction (mem_getLabel m). simpl. trivial.
Qed.
  rewrite <- (subst_distr_mem_getLabel z H m) in H1.


  assert ((map mem_getLabel ms) = (map (fun x : mem => mem_getLabel ([z ~mem> u]x)) ms)) as Heqs.
  apply map_ext.
  intros.
  apply subst_distr_mem_getLabel. assumption.

  rewrite <- Heqs in H1. clear Heqs.
  auto.
Qed.


Lemma x_notin_fv_subst_x: forall z u t,
   z \notin fv_tm u
-> z \notin fv_tp ([z ~tp> u]t).
Proof.
  introv NI.
  destructs (fv_intro_subst u NI). trivial.
Qed.
 

Lemma subst_preserves_fv_tp: forall x z u t,
   x <> z
-> x \notin fv_tm u
-> x \notin fv_tp t -> x \notin fv_tp ([z ~tp> u]t).
Proof.
  introv Neq ZNotInU.
  destructs (fv_intro_subst_2 u Neq ZNotInU). apply H1; trivial.
Qed.

   
Lemma subst_preserves_notin_env: forall (v z: var) E u U H,
   v # E & z ~ U & H
->   v # E & ([z ~env> u]H).
  intros.
  induction H; try destruct a; simpl in *; env_fix; auto*.
    assert (v # (E & z ~ U & H)) by auto.
    pose (IHlist H1).
    notin_simpl; auto*.
Qed.

Lemma fresh_env_elim_subst: forall x z u U E H,
    x <> z
->  x # E & ([z ~env> u]H)
->  x # E & z ~ U & H.
Proof.
  intros.
  assert (x # E) by auto*.
  assert (x # (z ~ U)) by auto*.
  assert (x # H) by auto*.
  auto*.
Qed.

Lemma subst_preserves_stable: forall z u t,
   stable t
-> stable u
-> lc_tm u
-> stable ([z ~> u]t).
Proof.
  intros. induction H; simpl in *; auto*.
  destruct (v == z); auto*.
Qed.

Lemma subst_preserves_not_singleton: forall z u T,
 lc_tm u
-> (forall p : tm, T <> tp_single p)
-> (forall p : tm, [z ~tp> u]T <> tp_single p).
Proof.
  intros. induction T; simpl in *; auto*; try discriminate.
Qed.



Lemma typing_subst : forall U E z u, 
    lc_tm u
 -> E |= u ~: U 
 -> stable u (*only needed when typing derivation was by typing_sel_single or typing_single: need to weaken this hypothesis?*)
 -> (forall G t T,
      G |= t ~: T -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~> u]t ~: [z ~tp> u]T) /\
    (forall G T,
      G |= T ~::Struct -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~tp> u] T ~::Struct ) /\
    (forall G T,
      G |= T ~::Concrete -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~tp> u] T ~::Concrete ) /\
    (forall G T R,
      G |= T ~< R -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~tp> u] T ~< [z ~tp> u] R  ) /\
    (forall G,
      wf_env G -> forall F, wf_env (E & z ~ U & F) -> wf_env (E & ([z ~env> u]F)) ) /\
    (forall G m,
      G |= m ~:::wf -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~mem> u]m ~:::wf) /\
    (forall G ms,
      G |= ms ~:::wfs -> forall F, G = E & z ~ U & F -> E & ([z ~env> u]F) |= [z ~mems> u]ms ~:::wfs).
Proof.
  introv LcU Typu StableU. apply typing_wf_mutual_ind; intro H; intros; subst; simpl.

  case_var.
    binds_get b. apply wf_env_implies_ok; trivial.
    (*  U cannot contain z: since wf_env(E & z ~ U & F), z must not occur in E *)
      destruct (subst_fresh z u) as [_ [EqSubst _]]. 
      destruct (typing_fresh z) as [TypFr _].
      destruct (TypFr E u U Typu (fresh_mid E F U w)) as [_ TypFrTp].
      rewrite (EqSubst U TypFrTp). clear EqSubst.
 
      assert (wf_env (E & ([z ~env> u]F))) as HWf. apply H0; auto*. clear H0.
      destruct (typing_weaken E ([z ~env> u]F)) as [Hweaken _]. 
      apply (Hweaken E u U Typu empty); auto*.

    binds_cases b. 
      (*case x not in F, thus T cannot depend on z*)
      assert (z # E).  apply (fresh_mid E F U w).
      assert (z \notin fv_tp T) as ZnotinT. 
      pose (@wf_env_remove2 _ (z ~ U) (@wf_env_remove2 _ F w)).
      apply (@wf_env_inv_type_dep E x T z); trivial.
      destruct (subst_fresh z u) as [_ [EqSubst _]]. 
      rewrite (EqSubst T ZnotinT). clear EqSubst.
      assert (wf_env (E & ([z ~env> u]F))) by auto.
      auto*.

      (*case x in F, thus T may depend on z*)
      apply* typing_var. 
        destruct (subst_lc z LcU) as [_ [RewLc _]]. auto.

(**)
  eapply typing_sel.
  simpl in H0. eapply H0. auto*. 

  fold (subst_mems z u mems).
  apply subst_distr_lookup; assumption.
  destruct (@subst_lc z u LcU) as [_ [Hlc _]].
  apply Hlc; assumption.

(*sel_single*)
  destruct (subst_open_rec tgt z LcU) as [_ [HSubst _]]. 
  rewrite (HSubst T 0).
  eapply typing_sel_single. simpl in H0. env_fix. eapply H0; auto*.

  fold (subst_mems z u mems).
  apply subst_distr_lookup; assumption.
  apply subst_preserves_stable; trivial.
  
(* single *)
  eapply typing_single. eapply H0; eauto.
  apply subst_preserves_stable; trivial.

(**)
  apply typing_new with (R:=  [z ~tp> u](tp_struct None ms)) (ms:= [z ~mems> u] ms).
  simpl.

  fold (subst_mems z u ms).
  apply subst_preserves_not_singleton; trivial.
  simpl in H0. env_fix. apply H0; trivial.
  simpl. fold (subst_mems z u ms). trivial.
  simpl in H1. env_fix. apply H1; trivial.
  apply (H2 F). trivial.

(* wf_single *)
  eapply wf_single; eauto. simpl in H2. eapply H2; trivial.

(**)
  apply wf_struct_self with (L:= {{z}} \u H). 
  intros.
  assert ( E & z ~ U & F & x ~ SelfTp = E & z ~ U & (F & x ~ SelfTp)) as HEq by auto*.
  assert ( x \notin H ) as HNI by auto*.
  pose (Hwfs:= H0 x HNI (F & x ~ SelfTp) HEq). 
  simpl in Hwfs. simpl.
  assert ( [z ~mems> u]open_mems ms x =  open_mems ([z ~mems> u]ms) x) as HEqs.
  assert (x <> z) as XneZ by auto*.
  destruct (@subst_open_var _ z x XneZ LcU) as [_ [_ [_ SubstMems]]].
  symmetry. apply SubstMems.

  fold (subst_mems z u ms).
  rewrite <- HEqs. assumption.

  destruct (@subst_lc z u LcU) as [_ [Hlc _]].
  apply Hlc; assumption.

(**)
  apply (H1 F); auto*.
  apply wf_struct_noself.
  simpl in *. apply H0; auto*.

(**)
  apply concrete_struct; auto*. 
  inversions* l.
  apply_fresh lc_struct_noself as x.  assert (x \notin L) as FrL by auto*. 
  fold (open_mems (map (subst_mem z u) ms) x). fold ([z ~mems> u] ms).
  pose (H1 x FrL). 
  fold (open_mems ms x) in l1.
  assert (x <> z) as XdiffZ by auto*.
  destruct (@subst_open_var u z x XdiffZ LcU) as [_ [_ [_ HSubst]]].
  rewrite (HSubst ms). clear HSubst.
  destruct (@subst_lc z u LcU) as [_ [_ [_ HSubstLc]]].
  apply (HSubstLc (open_mems ms x)); trivial.
  
  rewrite map_map. apply under_forAll_map with (f:= concrete_mem) (g:= (fun x : mem => concrete_mem ([z ~mem> u]x))).
  intros. inversions* H. simpl. apply concrete_mem_tm. destruct (@subst_lc z u LcU) as [HSubstLc _].
  apply (HSubstLc rhs); trivial.
  trivial.

(* expand tp_struct *)
  apply expand_struct.
  apply (H0 F); trivial.
  replace (tp_struct (option_map (subst_tp z u) o) (map (subst_mem z u) ms)) 
     with ([z ~tp> u](tp_struct o ms)) by auto.
  destruct (@subst_lc z u LcU) as [_ [HSubstLc _]].
  apply (HSubstLc (tp_struct o ms)); trivial.

(**) 
  eapply expand_single; eauto.

(*wf_env*)
  induction H.
  env_fix. simpl in *. env_fix.
  apply (wf_env_remove2 E (z ~ U)); trivial.
  simpl in *. destruct a. env_fix.
  pose (wf_env_remove2 (E & z ~ U & H) _ H0).
  pose (IHlist w).
  inversions H0.  simpl in *. env_fix.

  apply wf_env_cons; trivial.
    apply (subst_preserves_notin_env _ _  u U H H5). 

    intros. destruct (x == z). subst.
      destruct (typing_fresh z) as [TypFr _].
      assert (z # E) as ZFr by auto*.
      destruct (TypFr E u U Typu ZFr) as [ZFru _].
      apply (x_notin_fv_subst_x u t ZFru).
      pose (fresh_env_elim_subst u U E H n H1).
      pose (H6 x (fresh_env_elim_subst u U E H n H1)).  

      destruct (typing_fresh x) as [TypFrX _].
      assert (x # E) as XFr by auto*.
      destruct (TypFrX E u U Typu XFr) as [XFru _].
      apply (subst_preserves_fv_tp); trivial.


  apply (H0 F H1).


(**)
  apply wf_mem_mtm_rhs.
  apply H0;auto*.

(**)
  apply wf_mem_mtm_norhs.
  auto*. 
  destruct (@subst_lc z u LcU) as [_ [Hlc _]].
  apply Hlc; assumption.
  apply (H1 F); auto.

(**)
  auto*.

(**)
  simpl in *.
  apply wf_cons. auto*.
  apply subst_distr_memin; auto.
  apply H1. auto.

Qed.


Lemma mem_wf: forall E x R ms l mut rhs T,
    E & x ~ R |= open_mems ms x ~:::wfs
 -> option_has rhs (option_bind mem_getRhs (mems_lookup l ms))
 -> option_has T (ms ?: l)
 -> E & x ~ R |= (open_mem (mtm l mut T (Some rhs)) x) ~:::wf.
Proof.
  introv HRhs HCls.
  functional induction (mems_lookup l ms).
    contradiction.
    intro HClsMem.
    simpl in *.
    functional induction (mem_getRhs m'). simpl in *. inversion HRhs. unfold open_mem. simpl. 
    rewrite <- _x in H1.     rewrite <- HClsMem in H1.
    induction o. 
      simpl in HCls. subst rhs.  exact H1.
      contradiction.
    intro HHas. apply IHo. inversion HRhs. assumption. assumption. assumption.
Qed.


Lemma pres_stable: forall t t',
   stable t
-> t ~=> t'
-> stable t'.
Proof.
  introv Stable. gen t'. induction Stable; introv  Red; inversion Red; simpl in *; auto*.
  subst. (* TODO: this lemma is not provable as-is... 
            need to adapt evaluation/well-formedness so that right-hand sides are paths when a member selection is
            replaced by that rhs*)
Admitted.


Lemma pres_type_equality: forall E t t' u T,
   t ~=> t'
-> E |= u ~: {0 ~tp> t'}T
-> E |= u ~: {0 ~tp> t}T.
Admitted.

Lemma preservation_result : preservation.
Proof.
  introv Typ. gen t'.
  induction Typ; introv Red; inversions Red.
  
(* mems are well-formed by inverting the typing derivation of `new T0`*)
Lemma pres_mem_sel: forall E T0 o mems T l ms rhs,
   E |= new T0 ~: tp_struct o mems
-> option_has T (mems ?: l)
-> rt_expand T0 ms
-> option_has rhs (option_bind mem_getRhs (mems_lookup l ms))
-> E |= rhs ^^ new T0 ~: {0 ~tp> new T0}T.
Proof.
  introv Typ H H4 H6.
  inversion Typ. subst.  inversion H4 (*rt_expand*). subst. clear H4.
  inversion H5. subst. (*E |= tp_struct _ _ ~< tp_struct _ _ *)
  inversion H8. subst.  clear H8. (* ~::Concrete *)
  inversion H10 (* ~::Struct *). inversion H13. clear H10. subst.
  inversion H2. subst.
  set ( R := (tp_struct None ms0) ) in *.

  pick_fresh x. assert (x \notin L) as FrX by  auto.
  pose (Hwfmem:= mem_wf _ _ _ _ (H8 x FrX) H6 H).
  inversion Hwfmem. (* --> H9 : E & x ~ R |= {0 ~> x}rhs ~: {0 ~tp> x}T *)

  destruct (@typing_subst R E x (new R) (lc_new H4) Typ) as [SubstTm _].
  auto.
  pose (HSub:= SubstTm _ _ _ H10 empty).

  assert (x \notin (fv_tm rhs)) as XnotinRhs by auto*.
  pose (HSubIntro:= subst_intro_tm _ XnotinRhs (lc_new H4)).
  unfold open in HSubIntro.  rewrite <- HSubIntro in HSub.
  simpl in HSub. fold ( rhs ^^ new R) in HSub.
  assert (x \notin (fv_tp T)) as XnotinT by auto*.
  pose (HSubIntroTp:= subst_intro_tp _ XnotinT (lc_new H4)).
  unfold open_tp in HSubIntroTp.  rewrite <- HSubIntroTp in HSub. 
  apply HSub; trivial.
Qed.

  assert (E |= rhs ^^ new T0 ~: {0 ~tp> new T0}T) as HSub by (eapply pres_mem_sel; eauto).

  destruct (open_rec_lc (new T0)) as [_ [HOpenLc _]].
  rewrite (HOpenLc T H0 0) in HSub. 
  trivial.

(* *)
  pose (TypTgt:= IHTyp tgt' H4). auto*.


(* typing_sel_single *)
  eapply pres_mem_sel; eauto.

  pose (TypTgt:= IHTyp tgt' H4). 
  assert (E |= sel tgt' l ~: {0 ~tp> tgt'}T). eapply typing_sel_single; eauto.
  eapply pres_stable; eauto.

  eapply pres_type_equality; eauto.

  pose (IHTyp _ Red). assert ( E |= rhs ^^ new T0 ~: tp_single (rhs ^^ new T0)). eapply typing_single; eauto. eapply pres_stable; eauto.
  replace (tp_single (rhs ^^ new T0)) with ({0 ~tp> (rhs ^^ new T0)} tp_single (bvar 0))  in H3 by auto*.
  replace (tp_single (sel (new T0) l)) with ({0 ~tp> (sel (new T0) l)} tp_single (bvar 0)) by auto*.
  eapply pres_type_equality; eauto.

  pose (IHTyp _ Red). assert (  E |= sel tgt' l ~: tp_single (sel tgt' l)) by (eapply typing_single; eauto; eapply pres_stable; eauto).
  replace (tp_single (sel tgt' l)) with ({0 ~tp> (sel tgt' l)} tp_single (bvar 0)) in H1 by auto*.
  replace (tp_single (sel tgt l)) with ({0 ~tp> (sel tgt l)} tp_single (bvar 0)) by auto*.
  eapply pres_type_equality; eauto.
Qed. 
  

Lemma progress_result : progress.
Proof.
  introv Typ. gen_eq (empty : env) as E. poses Typ' Typ.
  induction Typ; intros; subst.
  contradictions.
  right.  destruct IHTyp. assumption. trivial. inversion H1. subst.
  assert (rt_expand T0 mems).
  induction T0. inversion Typ. apply rt_expand_struct.
  assert (exists rhs, option_has rhs (option_bind mem_getRhs (mems_lookup l mems))).
  rename H into HasMemL.
  inversion Typ. inversion H6. subst. inversions* H14.
  rename H12 into MemsConcrete.
  inversions* H4. 
  clear H0 H10 H6 H8 H11 H14 H12 H15 H4 H2 Typ Typ' H1 H3.

  (*ugh, messy!*)

(* cleaned up to:
  l : lab
  T : tp
  ms : list mem
  HasMemL : option_has T (ms ?: l)
  MemsConcrete : list_forAll (map concrete_mem ms)
  ============================
   exists rhs : tm,
     option_has rhs (option_bind mem_getRhs (mems_lookup l ms))
*)

  functional induction (mems_lookup l ms).
    contradiction.
    simpl in *. destruct MemsConcrete. inversion H. exists rhs. simpl. trivial.
    simpl in MemsConcrete. destruct MemsConcrete. apply IHo; assumption.

  destruct H4. (* eliminate existential *)

  exists (x ^^ new T0).
  auto*.

  destruct H1. auto*.
  left*. destruct typing_regular as [Hreg _]. pose (Hreg _ _ _ Typ'). destructs a. auto*.
Qed.

(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U"  "-I" "../lib" "-I" "../metatheory") ***
*** End: ***
*)